ds:x:Id fp Type, da:k:Knd fp Type, upd:update-spec(ds;da), k:Knd, x:Id.
update-spec-dom(upd;k;x)   

latex

Definitions	update-spec(ds;da), update-spec-dom(upd;k;x), x  dom(f), product-deq(A;B;a;b), KindDeq, <a, b>, Top, type List, , State(ds), x:AB(x), Valtype(da;k), t.1, f(x)?z, IdDeq, t.2, x.A(x), Void, x:A  B(x), Knd, a:A fp B(a), x:A. B(x), x. t(x), Type, t  T, Id
Lemmas	Id wf, fpf wf, Knd wf, pi2 wf, id-deq wf, fpf-cap wf, pi1 wf, ma-valtype wf, decl-state wf, nat wf, fpf-trivial-subtype-top, Kind-deq wf, product-deq wf, fpf-dom wf